Programmbeweis (Correctness Proof) Induktive mathematische Methode, die die Korrektheit von Programmen beweist. Dies ist insbesondere für Wiederholungsstrukturen aufwendig und schwierig. Bisher wurde diese Methode nur für kleine, sicherheitskritische Programme (z. B. in der Prozessdatenverarbeitung) angewendet.